Nuprl Lemma : unique_set_wf
9,38
postcript
pdf
T
:Type,
P
:(
T
). {!
x
:
T
|
P
(
x
)}
Type
latex
ProofTree
Definitions
P
Q
,
P
Q
,
x
(
s
)
,
{!
x
:
T
|
P
(
x
)}
,
t
T
,
,
x
:
A
.
B
(
x
)
origin
T:Type, P:(T
). {!x:T | P(x)} 
Type
T:Type, P:(T). {!x:T | P(x)} Type
Q
Q Tx:A. B(x)